Inference at * 1 2 
Iof proof for Lemma connex iff trichot:



1. T : Type
2. R : TT
3. a, b:T. Dec(R(a,b))
4. a, b:T. (R(a,b) & (R(b,a)))  (R(a,b) & R(b,a))  (R(b,a) & (R(a,b)))
5. x : T
6. y : T
  R(x,y)  R(y,x) 

latex

 by (% This side doesn't need decidability % 
((((InstHyp [x;y] 4) 
(CollapseTHENM (ProveProp))) 

(CoCollapseTHENA ((Auto_aux (first_nat 1:n) ((first_nat 1:n),(first_nat 3:n)) (first_tok :t
(C) inil_term)))) 

latex

(C.

Definitions

t  T, P  Q, x(s1,s2), P & Q, x:A. B(x),